(module substitutions  (lib "eopl.ss" "eopl")
  (require "drscheme-init.scm")
  (require "lang.scm")
  (require "data-structures.scm")
  
  (provide substitution? empty-subst extend-subst apply-subst-to-type)
  
  ;;;;;;;;;;;;;;;; Unit substitution ;;;;;;;;;;;;;;;;
  
  ;; apply-one-subst: type * tvar * type -> type
  ;; (apply-one-subst ty0 var ty1) returns the type obtained by
  ;; substituting ty1 for every occurrence of tvar in ty0.  This is
  ;; sometimes written ty0[tvar=ty1]
  ;; f(t) = Q(??)                   tx = ty + f(t)
  ;; tvar   ty0                               ty1
  ;; to use ty0 in stead of using ty1 in the right equation
  
  (define apply-one-subst
    (lambda (ty0 tvar ty1)
      (cases type ty0
        (proc-type (arg-type result-type) ;;"("  type  "->"  type  ")"
                   (proc-type
                    (apply-one-subst arg-type tvar ty1)
                    (apply-one-subst result-type tvar ty1)))
        (tvar-type (sn) ;;???????????????????????????????????????????????????????????????????????????????what is "sn" here?
                   (if (equal? ty0 tvar) ty1 ty0))
        (else ty0))))
  ;; the return is a type
  
  ;;;;;;;;;;;;;;;; Substitutions ;;;;;;;;;;;;;;;;
  
  ;; a substitution is a map from unknown types to types.
  ;; we'll represent this as an association list.
  
  (define pair-of
    (lambda (pred1 pred2)
      (lambda (val)
        (and (pair? val) (pred1 (car val)) (pred2 (cdr val))))))
  
  (define substitution? 
    (list-of (pair-of tvar-type? type?)));;a substitution is composed of "type variable" and "type"
  
  ;; basic observer: apply-subst-to-type
  ;; apply-subst-to-type : type * subst -> type
  ;; this is sometimes written ty1.subst
  
  (define apply-subst-to-type
    (lambda (ty subst)
      (cases type ty
        (int-type () (int-type))
        (bool-type () (bool-type))
        (void-type () (void-type))        
        (proc-type (t1 t2)
                   (proc-type
                    (apply-subst-to-type t1 subst)
                    (apply-subst-to-type t2 subst)))
        ;;        (list-type (ty) (list 'listof (type-to-external-form ty)))
        (list-type (type) (list-type (apply-subst-to-type type)))
        ( refto-type (type)
                     (refto-type (apply-subst-to-type type)
                                 ))        
        (tvar-type (sn)
                   (let ((tmp (assoc ty subst)))
                     (if tmp
                         (cdr tmp)
                         ty)))
        )))
  
  ;; empty-subst : () -> subst
  ;; produces a representation of the empty substitution.
  
  (define empty-subst (lambda () '()))
  
  ;; extend-subst : subst * tvar * type -> subst
  
  ;; (extend-subst s tv t) produces a substitution with the property
  ;; that for all t0,
  
  ;;   (apply-subst t0 (extend-subst s tv t))
  ;;   = (apply-one-subst (apply-subst t0 s) tv t)
  
  ;; i.e.,  t0.(s[tv=t]) = (t0.s)[tv=t]
  
  ;; this means that for any type variable tv0 in the domain of s,
  
  ;;   (apply-subst tv0 (extend-subst s tv t))
  ;;   = (apply-one-subst (apply-subst tv0 s) tv t)
  
  ;; so we extend the substitution with a new element, and apply [t/v] to every
  ;; element already in the substitution. 
  
  (define extend-subst
    (lambda (subst tvar ty)
      (cons
       (cons tvar ty)
       (map 
        (lambda (p)
          (let ((oldlhs (car p))
                (oldrhs (cdr p)))
            (cons
             oldlhs
             (apply-one-subst oldrhs tvar ty))))
        subst))))
  )